\begin{tabbing}
1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. $\forall$$b$:($T$ List). ($\parallel$$v$$\parallel$ = $\parallel$$b$$\parallel$) $\Rightarrow$ ($\forall$$i$:$\mathbb{N}$. ($i$ $<$ $\parallel$$v$$\parallel$) $\Rightarrow$ ($v$[$i$] = $b$[$i$])) $\Rightarrow$ ($v$ = $b$)
\\[0ex]6. $T$ List
\\[0ex]7. $u_{1}$ : $T$
\\[0ex]8. $v_{1}$ : $T$ List
\\[0ex]9. \=($\parallel$[$u$ / $v$]$\parallel$ = $\parallel$$v_{1}$$\parallel$)\+
\\[0ex]$\Rightarrow$ ($\forall$$i$:$\mathbb{N}$. ($i$ $<$ $\parallel$[$u$ / $v$]$\parallel$) $\Rightarrow$ ([$u$ / $v$][$i$] = $v_{1}$[$i$]))
\\[0ex]$\Rightarrow$ ([$u$ / $v$] = $v_{1}$)
\-\\[0ex]10. $\parallel$$v$$\parallel$+1 = $\parallel$$v_{1}$$\parallel$+1
\\[0ex]11. $\forall$$i$:$\mathbb{N}$. ($i$ $<$ ($\parallel$$v$$\parallel$+1)) $\Rightarrow$ ([$u$ / $v$][$i$] = [$u_{1}$ / $v_{1}$][$i$])
\\[0ex]12. $i$ : $\mathbb{N}$
\\[0ex]13. $i$ $<$ $\parallel$$v$$\parallel$
\\[0ex]$\vdash$  $v$[$i$] = $v_{1}$[$i$]
\end{tabbing}